\begin{tabbing}
$\forall$${\it es}$:ES, $e$:E.
\\[0ex]isrcv($e$)
\\[0ex]$\Rightarrow$ (\=index($e$) $=$ 0\+
\\[0ex]$\Leftrightarrow$
\\[0ex](\=$\forall$${\it e'}$:E.\+
\\[0ex]isrcv(${\it e'}$) $\Rightarrow$ sender(${\it e'}$) $=$ sender($e$) $\in$ E $\Rightarrow$ lnk($e$) $=$ lnk(${\it e'}$) $\in$ IdLnk $\Rightarrow$ $e$ $\leq$ ${\it e'}$ ))
\-\-
\end{tabbing}